(VERS0 0 NIL NIL ((WISEMEN (#& . 0) (#& . 11) (#& . 30) (#& . 37) (#& . 46) (#& . 50) (#& . 54)) (KNOWAX (#& . 55) (#& . 58) (#& . 32) (#& . 39) (#& . 52) (#& . 35) (#& . 42) (#& . 48) (#& . 15) (#& . 4) (#& . 45) (#& . 61) (#& . 62) (#& . 63) (#& . 64) (#& . 65) (#& . 66) (#& . 67) (#& . 68) (#& . 69) (#& . 70) (#& . 71) (#& . 72) (#& . 73) (#& . 74) (#& . 75))) ((((∀ S P)) (TRUE1 (* /0 (EQUIV1 ($ S P) (OR1 (* S P) (* S (NOT1 P))))))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (* /0 (EQUIV1 ($ S P) (OR1 (* S P) (* S (NOT1 P)))))))) . NIL . ((EQUIV1 #& . 56) (NOT1 #& . 51) (TRUE1 #& . 34) (* #& . 41) ($ #& . 47) (P #& . 22) (S #& . 7) (/0 #& . 44)) . ((OR1 #& . 38)) . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 26 .) ((((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (NOT1 (* S P)) (* S (NOT1 (* S P))))))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (NOT1 (* S P)) (* S (NOT1 (* S P)))))))) . NIL . ((IMPLIES1 #& . 59) (NOT1 #& . 51) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (S #& . 7) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 25 .) ((((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* S P) (* S (* S P)))))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* S P) (* S (* S P))))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (S #& . 7) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 24 .) ((((∀ P)) (TRUE1 (* /0 (IMPLIES1 (NOT1 (NOT1 P)) P)))) . (AXIOM (TM& ((∀ P)) (TRUE1 (* /0 (IMPLIES1 (NOT1 (NOT1 P)) P))))) . NIL . ((IMPLIES1 #& . 59) (NOT1 #& . 51) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 23 .) ((((∀ P Q R)) (TRUE1 (* /0 (IMPLIES1 (AND1 (IMPLIES1 R (IMPLIES1 P Q)) (IMPLIES1 R P)) (IMPLIES1 R Q))))) . (AXIOM (TM& ((∀ P Q R)) (TRUE1 (* /0 (IMPLIES1 (AND1 (IMPLIES1 R (IMPLIES1 P Q)) (IMPLIES1 R P)) (IMPLIES1 R Q)))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (R #& . 26) (Q #& . 24) (P #& . 22) (/0 #& . 44)) . ((AND1 #& . 31)) . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 22 .) ((((∀ P Q)) (TRUE1 (* /0 (IMPLIES1 P (IMPLIES1 Q P))))) . (AXIOM (TM& ((∀ P Q)) (TRUE1 (* /0 (IMPLIES1 P (IMPLIES1 Q P)))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (Q #& . 24) (P #& . 22) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 21 .) ((((∀ S P Q)) (TRUE1 (* /0 (IMPLIES1 (AND1 (* S P) (* S (IMPLIES1 P Q))) (* S Q))))) . (AXIOM (TM& ((∀ S P Q)) (TRUE1 (* /0 (IMPLIES1 (AND1 (* S P) (* S (IMPLIES1 P Q))) (* S Q)))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (Q #& . 24) (P #& . 22) (S #& . 7) (/0 #& . 44)) . ((AND1 #& . 31)) . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 20 .) ((((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* /0 P) (* /0 (* S P)))))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* /0 P) (* /0 (* S P))))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (S #& . 7) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 19 .) ((((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* S P) P)))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (* /0 (IMPLIES1 (* S P) P))))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (S #& . 7) (/0 #& . 44)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 18 .) ((((∀ S P)) (TRUE1 (IMPLIES1 (* S P) P))) . (AXIOM (TM& ((∀ S P)) (TRUE1 (IMPLIES1 (* S P) P)))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (* #& . 41) (P #& . 22) (S #& . 7)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 17 .) ((((∀ P Q)) (≡ (TRUE1 (EQUIV1 P Q)) (≡ (TRUE1 P) (TRUE1 Q)))) . (AXIOM (TM& ((∀ P Q)) (≡ (TRUE1 (EQUIV1 P Q)) (≡ (TRUE1 P) (TRUE1 Q))))) . NIL . ((EQUIV1 #& . 56) (TRUE1 #& . 34) (Q #& . 24) (P #& . 22)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 16 .) ((((∀ P)) (≡ (TRUE1 (NOT1 P)) (¬ (TRUE1 P)))) . (AXIOM (TM& ((∀ P)) (≡ (TRUE1 (NOT1 P)) (¬ (TRUE1 P))))) . NIL . ((NOT1 #& . 51) (TRUE1 #& . 34) (P #& . 22)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 15 .) ((((∀ P Q)) (⊃ (≡ (TRUE1 (IMPLIES1 P Q)) (TRUE1 P)) (TRUE1 Q))) . (AXIOM (TM& ((∀ P Q)) (⊃ (≡ (TRUE1 (IMPLIES1 P Q)) (TRUE1 P)) (TRUE1 Q)))) . NIL . ((IMPLIES1 #& . 59) (TRUE1 #& . 34) (Q #& . 24) (P #& . 22)) . NIL . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 14 .) ((((∀ P Q)) (≡ (TRUE1 (OR1 P Q)) (∨ (TRUE1 P) (TRUE1 Q)))) . (AXIOM (TM& ((∀ P Q)) (≡ (TRUE1 (OR1 P Q)) (∨ (TRUE1 P) (TRUE1 Q))))) . NIL . ((TRUE1 #& . 34) (Q #& . 24) (P #& . 22)) . ((OR1 #& . 38)) . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 13 .) ((((∀ P Q)) (≡ (TRUE1 (AND1 P Q)) (∧ (TRUE1 P) (TRUE1 Q)))) . (AXIOM (TM& ((∀ P Q)) (≡ (TRUE1 (AND1 P Q)) (∧ (TRUE1 P) (TRUE1 Q))))) . NIL . ((TRUE1 #& . 34) (Q #& . 24) (P #& . 22)) . ((AND1 #& . 31)) . NIL . ((&& . 1)) . NIL . KNOWAX . NIL . NIL . 12 .) (10 . | IMPLIES1 | . INFIX . 840 .) (CONSTANT . ((PROPOSITION PROPOSITION) . PROPOSITION) . UNIVERSAL . NIL . (#& . 60) . (#& . 58) . IMPLIES1 .) (NIL . (DECL (IMPLIES1) (OT& (PROPOSITION PROPOSITION) . PROPOSITION) CONSTANT NIL INFIX 840) . NIL . ((IMPLIES1 #& . 59)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 2 .) (8 . | EQUIV1 | . INFIX . 830 .) (CONSTANT . ((PROPOSITION PROPOSITION) . PROPOSITION) . UNIVERSAL . NIL . (#& . 57) . (#& . 55) . EQUIV1 .) (NIL . (DECL (EQUIV1) (OT& (PROPOSITION PROPOSITION) . PROPOSITION) CONSTANT NIL INFIX 830) . NIL . ((EQUIV1 #& . 56)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 1 .) ((TRUE1 (* WISE3 (NOT1 (* WISE2 WHITE2)))) . (AXIOM (TM& TRUE1 (* WISE3 (NOT1 (* WISE2 WHITE2))))) . NIL . ((NOT1 #& . 51) (TRUE1 #& . 34) (* #& . 41) (WISE2 #& . 10) (WISE3 #& . 1) (WHITE2 #& . 29)) . NIL . NIL . ((&& . 1)) . NIL . WISEMEN . NIL . NIL . 7 .) (5 . |NOT1 | . UNARY . 870 .) (NIL . (DECL (NOT1) (OT& (PROPOSITION) . PROPOSITION) CONSTANT NIL UNARY 870) . NIL . ((NOT1 #& . 51)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 5 .) (CONSTANT . ((PROPOSITION) . PROPOSITION) . UNIVERSAL . NIL . (#& . 53) . (#& . 52) . NOT1 .) ((TRUE1 (* WISE3 (* WISE2 (NOT1 (* WISE1 WHITE1))))) . (AXIOM (TM& TRUE1 (* WISE3 (* WISE2 (NOT1 (* WISE1 WHITE1)))))) . NIL . ((NOT1 #& . 51) (TRUE1 #& . 34) (* #& . 41) (WISE2 #& . 10) (WISE1 #& . 2) (WISE3 #& . 1) (WHITE1 #& . 13)) . NIL . NIL . ((&& . 1)) . NIL . WISEMEN . NIL . NIL . 6 .) (1 . $ . INFIX . 875 .) (NIL . (DECL ($) (OT& (PERSON PROPOSITION) . PROPOSITION) CONSTANT NIL INFIX 875) . NIL . (($ #& . 47)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 8 .) (CONSTANT . ((PERSON PROPOSITION) . PROPOSITION) . UNIVERSAL . NIL . (#& . 49) . (#& . 48) . $ .) ((TRUE1 (* /0 (AND1 ($ WISE1 WHITE2) ($ WISE1 WHITE3) ($ WISE2 WHITE1) ($ WISE2 WHITE3) ($ WISE3 WHITE1) ($ WISE3 WHITE2)))) . (AXIOM (TM& TRUE1 (* /0 (AND1 ($ WISE1 WHITE2) ($ WISE1 WHITE3) ($ WISE2 WHITE1) ($ WISE2 WHITE3) ($ WISE3 WHITE1) ($ WISE3 WHITE2))))) . NIL . ((TRUE1 #& . 34) (* #& . 41) ($ #& . 47) (/0 #& . 44) (WISE2 #& . 10) (WISE1 #& . 2) (WISE3 #& . 1) (WHITE2 #& . 29) (WHITE1 #& . 13) (WHITE3 #& . 12)) . ((AND1 #& . 31)) . NIL . ((&& . 1)) . NIL . WISEMEN . NIL . NIL . 5 .) (NIL . (DECL (/0) (OT& . PERSON) CONSTANT PERSON) . NIL . ((/0 #& . 44) (PERSON #& . 3)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 11 .) (CONSTANT . PERSON . PERSON . NIL . NIL . (#& . 45) . /0 .) (1 . * . INFIX . 875 .) (NIL . (DECL (*) (OT& (PERSON PROPOSITION) . PROPOSITION) CONSTANT NIL INFIX 875) . NIL . ((* #& . 41)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 7 .) (CONSTANT . ((PERSON PROPOSITION) . PROPOSITION) . UNIVERSAL . NIL . (#& . 43) . (#& . 42) . * .) (5 . | OR1 | . INFIX . 850 .) (NIL . (DECL (OR1) (FT& ((PROPOSITION PROPOSITION) PROPOSITION NIL . PROPOSITION)) FUNCTIONAL NIL INFIX 850 BOTH) . NIL . NIL . ((OR1 #& . 38)) . NIL . NIL . NIL . KNOWAX . NIL . NIL . 4 .) (FUNCTIONAL . (((PROPOSITION PROPOSITION) PROPOSITION NIL . PROPOSITION)) . UNIVERSAL . BOTH . (#& . 40) . (#& . 39) . OR1 .) ((TRUE1 (* /0 (OR1 WHITE1 WHITE2 WHITE3))) . (AXIOM (TM& TRUE1 (* /0 (OR1 WHITE1 WHITE2 WHITE3)))) . NIL . ((TRUE1 #& . 34) (* #& . 41) (/0 #& . 44) (WHITE2 #& . 29) (WHITE1 #& . 13) (WHITE3 #& . 12)) . ((OR1 #& . 38)) . NIL . ((&& . 1)) . NIL . WISEMEN . NIL . NIL . 4 .) (6 . |TRUE1 | . UNARY . 820 .) (NIL . (DECL (TRUE1) (OT& (PROPOSITION) . TRUTHVAL) CONSTANT NIL UNARY 820) . NIL . ((TRUE1 #& . 34)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 6 .) (CONSTANT . ((PROPOSITION) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 36) . (#& . 35) . TRUE1 .) (6 . | AND1 | . INFIX . 860 .) (NIL . (DECL (AND1) (FT& ((PROPOSITION PROPOSITION) PROPOSITION NIL . PROPOSITION)) FUNCTIONAL NIL INFIX 860 BOTH) . NIL . NIL . ((AND1 #& . 31)) . NIL . NIL . NIL . KNOWAX . NIL . NIL . 3 .) (FUNCTIONAL . (((PROPOSITION PROPOSITION) PROPOSITION NIL . PROPOSITION)) . UNIVERSAL . BOTH . (#& . 33) . (#& . 32) . AND1 .) ((TRUE1 (AND1 WHITE1 WHITE2 WHITE3)) . (AXIOM (TM& TRUE1 (AND1 WHITE1 WHITE2 WHITE3))) . NIL . ((TRUE1 #& . 34) (WHITE2 #& . 29) (WHITE1 #& . 13) (WHITE3 #& . 12)) . ((AND1 #& . 31)) . NIL . ((&& . 1)) . NIL . WISEMEN . NIL . NIL . 3 .) (CONSTANT . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 11) . WHITE2 .) (11 . PROPOSITION . PREFIX . 1000 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . R1 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . R .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . Q1 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . Q .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . P1 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . P .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . P0 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . P2 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . Q0 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . Q2 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . R0 .) (VARIABLE . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 15) . R2 .) (NIL . (DECL (P P0 P1 P2 Q Q0 Q1 Q2 R R0 R1 R2) (OT& . PROPOSITION) VARIABLE PROPOSITION) . NIL . ((R2 #& . 16) (R0 #& . 17) (Q2 #& . 18) (Q0 #& . 19) (P2 #& . 20) (P0 #& . 21) (PROPOSITION #& . 14) (P #& . 22) (P1 #& . 23) (Q #& . 24) (Q1 #& . 25) (R #& . 26) (R1 #& . 27)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 9 .) (VARIABLE . ((PROPOSITION) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 28) . (#& . 15) . PROPOSITION .) (CONSTANT . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 11) . WHITE1 .) (CONSTANT . PROPOSITION . PROPOSITION . NIL . NIL . (#& . 11) . WHITE3 .) (NIL . (DECL (WHITE1 WHITE2 WHITE3) (OT& . PROPOSITION) CONSTANT PROPOSITION) . NIL . ((WHITE3 #& . 12) (WHITE1 #& . 13) (PROPOSITION #& . 14) (WHITE2 #& . 29)) . NIL . NIL . NIL . NIL . WISEMEN . NIL . NIL . 2 .) (CONSTANT . PERSON . PERSON . NIL . NIL . (#& . 0) . WISE2 .) (6 . PERSON . PREFIX . 1000 .) (VARIABLE . PERSON . PERSON . NIL . NIL . (#& . 4) . S1 .) (VARIABLE . PERSON . PERSON . NIL . NIL . (#& . 4) . S .) (VARIABLE . PERSON . PERSON . NIL . NIL . (#& . 4) . S0 .) (VARIABLE . PERSON . PERSON . NIL . NIL . (#& . 4) . S2 .) (NIL . (DECL (S S0 S1 S2) (OT& . PERSON) VARIABLE PERSON) . NIL . ((S2 #& . 5) (S0 #& . 6) (PERSON #& . 3) (S #& . 7) (S1 #& . 8)) . NIL . NIL . NIL . NIL . KNOWAX . NIL . NIL . 10 .) (VARIABLE . ((PERSON) . TRUTHVAL) . UNIVERSAL . NIL . (#& . 9) . (#& . 4) . PERSON .) (CONSTANT . PERSON . PERSON . NIL . NIL . (#& . 0) . WISE1 .) (CONSTANT . PERSON . PERSON . NIL . NIL . (#& . 0) . WISE3 .) (NIL . (DECL (WISE1 WISE2 WISE3) (OT& . PERSON) CONSTANT PERSON) . NIL . ((WISE3 #& . 1) (WISE1 #& . 2) (PERSON #& . 3) (WISE2 #& . 10)) . NIL . NIL . NIL . NIL . WISEMEN . NIL . NIL . 1 .))